(set-logic ALL)
(define-fun s2 () Int 50)
(define-fun s4 () Int 24)
(define-fun s7 () Int 2400)
(define-fun s9 () Int 30)
(define-fun s11 () Int 33)
(define-fun s14 () Int 2100)
(define-fun s17 () Int 75)
(define-fun s19 () Int 90)
(define-fun s21 () Int 95)
(declare-fun s0 () Int)
(declare-fun s1 () Int)
(declare-fun s26 () Int)
(define-fun s3 () Int (* s0 s2))
(define-fun s5 () Int (* s1 s4))
(define-fun s6 () Int (+ s3 s5))
(define-fun s8 () Bool (<= s6 s7))
(define-fun s10 () Int (* s0 s9))
(define-fun s12 () Int (* s1 s11))
(define-fun s13 () Int (+ s10 s12))
(define-fun s15 () Bool (<= s13 s14))
(define-fun s16 () Int (+ s0 s9))
(define-fun s18 () Bool (>= s16 s17))
(define-fun s20 () Int (+ s1 s19))
(define-fun s22 () Bool (>= s20 s21))
(define-fun s23 () Int (- s16 s17))
(define-fun s24 () Int (- s20 s21))
(define-fun s25 () Int (+ s23 s24))
(assert s8)
(assert s15)
(assert s18)
(assert s22)
(assert (= s25 s26))
(maximize s26)
(check-sat)
(get-value (s26))